(DEFPROP PARTIT 
	((LESSEQP M N)
	 (TACK X W) 
	 (PARTITION U N) 
	 (PART1 U V N) 
	 (TESTPART V U) 
	 (COMBINE W) 
	 (PARTIT U N) 
	 (PARTN U V N)
	 (LISTLIST U)
	 (PLISTP X)
	 (LISTP X)
	 (ISPARTIT V W N) 
	 (ISPARTN U V W N) 
	 (ISHEAD U V)
	 (TESTPARTIT U V N) )
        PARTITFNS)

(DEFUN LESSEQP (M N) (NOT (GREATERP M N)) )

(DEFUN TACK (X W) 
       (COND ((NULL W) NIL)
	     (T (CONS (CONS X (CAR W)) (TACK X (CDR W)))))) 

(DEFUN PARTITION (U N) 
       (COND ((LESSP (LENGTH U) N) '(INVALID N))
	     ((EQUAL N 1) (LIST (LIST U)))
	     (T (PART1 (LIST (CAR U)) (CDR U) (SUB1 N))) )) 

;;; |v|≥n≥1
(DEFUN PART1 (U V N) 
       (APPEND (TACK U (PARTITION V N))
	       (COND ((LESSEQP (LENGTH V) N) NIL)
		     (T	(PART1 (APPEND U (LIST (CAR V))) (CDR V) N)) ))) 

(DEFUN TESTPART (V U) 
       (COND ((NULL V) T)
	     ((AND (EQUAL (COMBINE (CAR V)) U)
		   (TESTPART (CDR V) U))))) 

(DEFUN COMBINE (W) 
       (COND ((NULL W) NIL) (T (APPEND (CAR W) (COMBINE (CDR W)))))) 


;;;Correctness of PARTITION
;;;∀u n.[|u|≥n ⊃ [wεpartition[u,n] ↔ |w|=n and combine w=u]]
;;;∀u n.[|u|≥n ⊃ ∀w.multiplicity[w,partition[u,n]] ≤ 1]


(DEFUN PARTIT (U N) 
  (COND ((ZEROP N) '|Can't make 0 partitions|)
	((GREATERP N (LENGTH U)) '|List too short|)
	((EQ N 1) (LIST (LIST U)))
	(T (PARTN (LIST (CAR U)) (CDR U) (SUB1 N))) ))

(DEFUN PARTN (U V N)
  (COND ((GREATERP N (LENGTH V)) NIL)
	((EQ N 0) NIL)
	((EQ N 1) (APPEND (TACK U (LIST (LIST V))) 
			  (PARTN (APPEND U (LIST (CAR V))) (CDR V) N)))
	(T (APPEND (TACK U (PARTN (LIST (CAR V)) (CDR V) (SUB1 N)))
	  	   (PARTN (APPEND U (LIST (CAR V))) (CDR V) N))) ))

(DEFUN LISTLIST (U) (OR (NULL U) (AND (PLISTP (CAR U)) (LISTLIST (CDR U)))))

(DEFUN PLISTP (X) (AND (NOT (NULL X)) (LISTP X)) )
(DEFUN LISTP (X) (OR (NULL X) (AND (NOT (ATOM X)) (LISTP (CDR X)))))

(DEFUN ISPARTIT (V W N) 
   (AND (EQ (LENGTH W) N)
        (LISTLIST W)
	(EQ (COMBINE W) V) ))

(DEFUN ISPARTN (U V W N) 
   (AND (ISPARTIT (APPEND U V) W (ADD1 N)) (ISHEAD U (CAR W)) ))

(DEFUN ISHEAD (U V)
 (OR (NULL U) (AND (NOT (NULL V)) (EQ (CAR U) (CAR V)) (ISHEAD (CDR U)(CDR V))) ))

(DEFUN TESTPARTIT (U V N) 
  (OR (NULL V) (AND (ISPARTIT U (CAR V) N) (TESTPARTIT U (CDR V) N)) ))